New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add injectivity annotations #9500
Conversation
Note: when we discussed this during a meeting, I suggested that you and @lpw25 write a short document that would explain, with examples, the current need for (and uses of) the feature (including the examples from Oleg, and the "injectivity witnesses" that @lpw25 mentioned). I think this would be very useful to follow what's going on -- I understand the general feature and I think agree with @lpw25 it is simple and nice to expose it, but I haven't been able to follow the recent practical interest in it. |
I think this means that #5985 can finally be closed. |
What's the situation with GADTs? I haven't looked at the implementation, but gave the branch a quick try and was surprised to discover that injectivity annotations for some indexes are rejected:
|
@yallop There is no point in giving injectivity annotations for "nominal" (i.e. records and sums, including GADTs and extensible ones) types: their parameters are always injective by definition. |
Understood. But since the annotations are correct, even if pointless, I think it's best to accept them when they're given. |
In particular, I think this behaviour, where a variant definition matches an injective signature, but can't be marked as injective directly, is surprising:
|
@yallop The last commit ignores injectivity annotations for nominal types, so this fixes your problem. |
You can see the injectivity witnesses people use here: I'm not sure whether any uses of it are in our open source code, but I think how you use it is fairly obvious. I'll try and dig up an example of why you might use it when I have some time. |
This PR is now ready for reviewing. It implements injectivity annotations on type parameters, using the suggested syntax The main motivation is solving the famous #5985, explained in my OCaml 2013 paper. In particular, this allows to define GADTs where parametric abstract types appear as index. See the nominal types RFC or Oleg's recent mail on the caml-list for examples of this problem. Injectivity annotations do not make sense for nominal types (records or sum types), since all their parameters are injective by definition. For them, annotations are silently ignored. For type abbreviations (public or private), the injectivity of parameters can be inferred from the body of the type, and annotations are only checked. For abstract types and private row types, injectivity annotations should be satisfied by the actual implementation. They are kept in the type definition, and checked through module subtyping. Note that for private row types, injectivity can also be inferred in some cases. For concrete examples, see the file The implementation has two parts.
|
@lpw25 Thank you, this is clear enough indeed. |
This PR is a bit strange, as most of the effort seems to be going into constrained type parameters in type abbreviations, which is a very minor feature. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a very welcome change!
I believe the code to be correct, but please see the comments attached to this review for some suggestions for small improvements to the interface, implementation and documentation.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The code looks correct to me and I'm in favour of the feature.
manual/manual/refman/typedecl.etex
Outdated
@@ -200,6 +208,18 @@ constraints, the variance properties of the type constructor | |||
are inferred from its definition, and the variance annotations are | |||
only checked for conformance with the definition. | |||
|
|||
Injectivity annotations only make sense for abstract types and private |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Injectivity annotations only make sense for abstract types and private | |
Injectivity annotations are only necessary for abstract types and private |
@garrigue this can be merged, but you need to fix conflicts first -- in the Changes, and in the generated parser. |
cc7cbc2
to
be9ec2a
Compare
See ocaml/ocaml#9500 for the introduction of the breaking change within OCaml.
See ocaml/ocaml#9500 for the introduction of the breaking change within OCaml.
See ocaml/ocaml#9500 for the introduction of the breaking change within OCaml.
Add injectivity annotations on abstract types, to allow using them in GADTs or constrained parameters.
The syntax is as suggested:
When combined with a variance, the variance comes first:
See examples in
testsuite/tests/typing-misc/injectivity.ml